Conal Elliott

The Reactive library implements functional reactive programming (FRP) in a data-driven and yet purely functional way, on top of a new primitive I call “unambiguous choice”, or unamb. This primitive has simple functional semantics and a concurrent implementation. The point is to allow one to try out two different ways to answer the same question, when it’s not known in advance which one will succeed first, if at all.

This post describes and demonstrates unamb and its implementation.

What’s unamb?

The value of a `unamb` b is the more defined of the values a and b. The operation is subject to a semantic precondition, which is that a and b must be equal unless one or both is bottom. It’s this precondition that distinguishes unamb from the ambiguous (nondeterministic) choice operator amb.

This precondition also distinguishes unamb from least upper (information) bound (“lub”). The two operators agree where both are defined, but lub is much more widely defined than unamb is. For instance, consider the pairs (1,⊥) and (⊥,2). The first pair has information only about its first element, while the second pair has information only about its second element. Their lub is (1,2). The triples (1,⊥,3) and (⊥,2,3) are also consistent and have a lub, namely (1,2,3).

Each of these two examples, however, violates unamb‘s precondition, because in each case the values are unequal and not ⊥.

In the examples below, I’ll use “⊥” in place of “undefined“, for brevity.

Parallel or

In spite of its limitation, unamb can do some pretty fun stuff. For instance, it’s easy to implement the famous “parallel or” operator, which yields true if either argument is true, even if one argument is ⊥.

por :: Bool -> Bool -> Bool
a `por` b = (a || b) `unamb` (b || a)

This use of unamb satisfies the precondition, because (||) is “nearly commutative”, i.e., commutative except when one ordering yields ⊥.

This game is useful with any nearly commutative operation that doesn’t always require evaluating both arguments. The general pattern:

parCommute :: (a -> a -> b) -> (a -> a -> b)
parCommute op x y = (x `op` y) `unamb` (y `op` x)

which can be specialized to parallel or and parallel and:

por :: Bool -> Bool -> Bool
por = parCommute (||)

pand :: Bool -> Bool -> Bool
pand = parCommute (&&)

Let’s see if por does the job. First, here’s sequential or:

*Data.Unamb> True || ⊥
True

*Data.Unamb> ⊥ || True
*** Exception: Prelude.undefined

Now parallel or:

*Data.Unamb> True `por` ⊥
True

*Data.Unamb> ⊥ `por` True
True

Short-circuiting multiplication

Another example is multiplication optimized for either argument being zero where the other might be expensive. Just for fun, we’ll optimize for an argument of one as well.

ptimes :: (Num a) => a -> a -> a
ptimes = parCommute times
 where
   0 `times` _ = 0
   1 `times` b = b
   a `times` b = a*b

There’s an important caveat: the type a must be flat. Otherwise, the precondition of unamb might not hold. While many Num types are flat, non-flat Num types are also useful, e.g., derivative towers and functions (and indeed, any applicative functor).

Testing:

*Data.Lub> 0 * ⊥
*** Exception: Prelude.undefined
*Data.Lub> ⊥ * 0
*** Exception: Prelude.undefined
*Data.Lub> ⊥ `ptimes` 0
0
*Data.Lub> 0 `ptimes` ⊥
0

Implementation

Let’s assume we had ambiguous choice

amb :: a -> a -> IO a

which applies to any two values of the same type, including fully defined, unequal values. Ambiguous choice nondeterministically chooses one or the other of the values, at its own whim, and may yield different results for the same pair of inputs.

Note that the result of amb is in IO because of its impure semantics. The resulting IO action might produce either argument, but it will only produce bottom if both arguments are bottom.

Given amb, unambiguous choice is easy to implement:

unamb :: a -> a -> a
a `unamb` b = unsafePerformIO (a `amb` b)

The unsafePerformIO is actually safe in this situation because amb is deterministic when the precondition of unamb satisfied.

The implementation of amb simply evaluates both arguments in parallel and returns whichever one finishes (reduces to weak head normal form) first. The racing happens via a function race, which works on actions:

race :: IO a -> IO a -> IO a

amb :: a -> a -> IO a
a `amb` b = evaluate a `race` evaluate b

(The actual definitions of unamb and amb are a bit prettier, for point-free fetishists.)

The race function uses some Concurrent Haskell primitives. For each action, race forks a thread that executes a given action and writes the result into a shared mvar. It then waits for the mvar to get written, and then halts the threads.

a `race` b = do v  <- newEmptyMVar
                ta <- forkPut a v
                tb <- forkPut b v
                x  <- takeMVar  v
                killThread ta
                killThread tb
                return x

forkPut :: IO a -> MVar a -> IO ThreadId
forkPut act v = forkIO (act >>= putMVar v)  -- naive version

This implementation of forkPut is a little too simplisitic. In Haskell, ⊥ doesn’t simply block forever; it raises an exception. That specific exception must be caught and neutralized.

forkPut act v = forkIO ((act >>= putMVar v) `catch` uhandler)
 where
   uhandler (ErrorCall "Prelude.undefined") = return ()
   uhandler err                             = throw err

Now when act evaluates ⊥, the exception is raised, the putMVar is bypassed, and then the exception is silenced. The result is that the mvar does not get written, so the other thread in race must win.

But, oops — what if the other thread also evaluates ⊥ and skips writing the mvar also? In that case, the main thread of race (which might be spun by another race) will block forever, waiting on an mvar that has no writer. This behavior would actually be just fine, since bottom is the correct answer. However, the GHC run-time system won’t stand for it, and cleverly raises an BlockedOnDeadMVar exception. For this reason, forkPut must neutralize a second exception via a second handler:

forkPut act v = forkIO ((act >>= putMVar v)
                        `catch` uhandler `catch` bhandler)
 where
   uhandler (ErrorCall "Prelude.undefined") = return ()
   uhandler err                             = throw err
   bhandler BlockedOnDeadMVar               = return ()

What’s next?

You can learn more about unamb on the unamb wiki page (where you’ll find links to the code) and in the paper Simply efficient functional reactivity.

My next post will show how to relax the stringent precondition on unamb into something more like the full least-upper-bound operation. This generalization supports richly structured (non-flat) types.

The Reactive library implements functional reactive programming (FRP) in a data-driven and yet purely functional way, on top of a new primitive I call “unambiguous choice”, or unamb. This primitive...